es:ES, a:Atom1, e:E. e sends a  Prop 

latex

Definitions	t  T, x:A. B(x), ES, Atom$n, E, P & Q, Type, AtomFree(T;x), P  Q, sender(e), s = t, val(e), valtype(e), x:T>>a, isrcv(e), b, x:AB(x), Prop, A & B, x:A. B(x), e receives a, e sends a
Lemmas	assert wf, es-isrcv wf, inheres wf, es-valtype wf, es-val wf, es-sender wf, es-E wf, event system wf, atom-free-es-valtype